Nuprl Lemma : fpf-type
11,40
postcript
pdf
A
:Type,
B
:(
A
Type),
f
:
a
:
A
fp
B
(
a
).
f
a
:{
a
:
A
| (
a
fpf-domain(
f
))} fp
B
(
a
)
latex
Definitions
x
:
A
.
B
(
x
)
,
a
:
A
fp
B
(
a
)
,
x
(
s
)
,
t
T
,
x
.
t
(
x
)
,
fpf-domain(
f
)
,
t
.1
,
S
T
,
suptype(
S
;
T
)
,
Lemmas
fpf
wf
,
list-subtype
,
l
member
wf
origin
A:Type, B:(A
Type), f:a:A fp B(a). f 
a:{a:A| (a fpf-domain(f))} fp B(a) A:Type, B:(AType), f:a:A fp B(a). f a:{a:A| (a fpf-domain(f))} fp B(a) x:A. B(x) B(a) T
x. t(x)
T